\begin{figure}[H]
\begin{tikzpicture}
\tikzset{font=\small,
	level 1+/.style={level distance=40pt},
	every tree node/.style={align=center, anchor=north},
	edge from parent/.style=
	{draw,
	 edge from parent path={(\tikzparentnode.south)
							-- +(0,-8pt)
							-| (\tikzchildnode)}}
}

\Tree [
.{\{pre\} keyAddition mid kid \{post\}}
	[.\node[draw]{unfold keyAddition};
		[.\node[draw]{eapply hoare\_seq};
			[.{\{pre\} mid[0][0] ::= \\ (mid[0][0] xor kid[0][0]) \{st$_1$\}}
				\node[draw]{apply hoare\_matrix\_xor\_00};
			]
			[.{\{st$_1$\} mid[0][1] ::= (mid[0][1] xor kid[0][1]); \ldots \{post\}}
				[.\node[draw]{eapply hoare\_seq};
					[.{\{st$_1$\} mid[0][1] ::= \\ (mid[0][1] xor kid[0][1]) \{st$_2$\}}
						\node[draw]{apply hoare\_matrix\_xor\_01};
					]
					[.{\{st$_2$\} mid[1][0] ::= \\ (mid[1][0] xor kid[1][0]); \ldots \{post\}}
						[.\node[draw]{eapply hoare\_seq};
							[.{\{st$_2$\} mid[1][0] ::= \\ (mid[1][0] xor kid[1][0]) \{st$_3$\}}
								\node[draw]{apply hoare\_matrix\_xor\_10};
							]
							[.{\{st$_3$\} mid[1][1] ::= \\ (mid[1][1] xor kid[1][1]) \{post\}}
								\node[draw]{apply hoare\_matrix\_xor\_11};
							]
						]
					]
				]
			]
		]
	]
]
\end{tikzpicture}
\caption{Árbol de prueba de hoare\_key\_addition} \label{tree:hoare_keyaddition}
\end{figure}